es:ES, T:Type, l1, l2:IdLnk, tg, a:Id, ds1, ds2:x:Id fp Type, P:(State(ds1)Prop),
Q:(State(ds2)Prop), f:(State(ds1)T).
weak-precond-send-p(es;T;;l1;tg;a;ds1;s,m. P(s,m) & (n:. n<m  P(s,n));f)
 weak-precond-send-p(es;;;l2;tg;a;ds2;s,m. Q(s,m) & (n:. n<m  Q(s,n));s,m. m)
 destination(l1) = source(l2)  Id
 destination(l2) = source(l1)  Id
 (s:State(ds1), k:. Dec(P(s,k)))
 (s:State(ds2), k:. Dec(Q(s,k)))
 (k:. @source(l1) stable s.P(s,k)  )
 (k:. @source(l2) stable s.Q(s,k)  )
 (k:.
 (e@source(l1).
 (P(state after e,k)  e'@destination(l1).Q((state when e'),k)  (n:. Q(state after e',n)))
 (e:E. kind(e) = rcv(l2,tg)  Knd  (k:. k<val(e)  P(state after e,k)))
 (k:, e:E.
 (kind(e) = rcv(l1,tg)  Knd  val(e) = f((state when sender(e)),k)  Q(state after e,k))
 e@destination(l1).True
 (k:. e@destination(l1).(n:k. Q((state when e),n))  (n:. Q(state after e,n))) 

latex

Definitions

, n-m, n+m, -n, ij, Dec(P), weak-precond-send-p(es;T;A;l;tg;a;ds;P;f), sender(e), kind(e), rcv(l,tg), <a,b>, A/x,y. B(x;y), locl(a), source(l), destination(l), T, Void, b, if b t else f fi, a<b, Knd, s ~ t, SQType(T), {T}, @i stable state.P(state)  , @i state ds, val(e), valtype(e), e@i. P(e), e@i.P(e), x:A. B(x), loc(e), (state when e), A & B, left+right, True, E, 1of(t), s = t, a:A fp B(a), Atom$n, IdLnk, ES, x:AB(x), P  Q, i  j < k, P & Q, {i..j}, #$n, x(s1,s2), Prop, x:AB(x), f(a), state after e, state@i, State(ds), {x:A| B(x) }, , AB, A, False, P  Q, vartype(i;x), f(x)?z, x. t(x), x:A. B(x), x.A(x), Type, Id, IdDeq, Top, t  T, Case b of inl(x)  s(x) ; inr(y)  t(y), lnk(e), e  e' , e c e', e'e.P(e'), P  Q, P  Q, (e <loc e'),

Lemmas

es-causle-le, es-le-causle, es-causle transitivity, es-le-total, decidable lt, es-valtype wf, member wf, not locl rcv, es-locl-iff, implies functionality wrt iff, all functionality wrt iff, stable-implies4, stable-implies3, decidable le, es-le-loc, es-rcv-kind, top wf, id-deq wf, Id wf, fpf-cap wf, es-vartype wf, subtype rel self, subtype rel dep function, es-state-after wf, nat wf, int seg wf, es-state-when wf, le wf, es-loc wf, es-val wf, es-state wf, es-state-type-implies, es-stable wf, Id sq, Knd sq, Knd wf, es-E wf, existse-at wf, alle-at wf, es-loc-rcv, es-loc-pred, IdLnk wf, true wf, squash wf, ldst wf, lsrc wf, es-kind-rcv, nat properties, rcv wf, es-kind wf, es-sender wf, decidable wf, decl-state wf, not wf, weak-precond-send-p wf, fpf wf, event system wf, ge wf